n:. 1  n = 1   

latex

Definitions	, tt, r * s, P & Q, , P  Q, P  Q, <+*>, 1, rxmn, t.2, t.1, e, ff, i <z j, if b then t else f fi , Y, (op,id) lb  i < ub. E(i), n x(op;id) e, n  e, e r n, r  n, False, A, A  B, i  j , P  Q, t  T, x:A. B(x),
Lemmas	qmul wf, exp unroll q, rationals wf, int-rational, ge wf, nat properties, nat wf